SMT solvers have been used successfully as reasoning engines for automatedverification and other applications based on automated reasoning. Currenttechniques for dealing with quantified formulas in SMT are generallyincomplete, forcing SMT solvers to report "unknown" when they fail to prove theunsatisfiability of a formula with quantifiers. This inability to returncounter-models limits their usefulness in applications that produce queriesinvolving quantified formulas. In this paper, we reduce these limitations byintegrating finite model finding techniques based on constraint solving intothe architecture used by modern SMT solvers. This approach is made possible bya novel solver for cardinality constraints, as well as techniques for on-demandinstantiation of quantified formulas. Experiments show that our approach iscompetitive with the state of the art in SMT, and orthogonal to approaches inautomated theorem proving.
展开▼
